\begin{tabbing}
$\forall$$A$:Type, $i$:$\mathbb{N}$, $L$:$A$ List.
\\[0ex]$i$+1$<\parallel$$L$$\parallel$
\\[0ex]$\Rightarrow$ (\=$\exists$$X$, $Y$:$A$ List.\+
\\[0ex]$L$ $=$ ($X$ @ [$L$[$i$]; $L$[$i$+1]] @ $Y$) \& swap($L$;$i$;$i$+1) $=$ ($X$ @ [$L$[$i$+1]; $L$[$i$]] @ $Y$) $\in$ $A$ List)
\-
\end{tabbing}